Power Programmierung/Power-Programmierung (Tewi)(1994).iso/magazine/drdobbs/1986/04/brownlst.apr

Text File | 1986-04-30 | 30KB | 961 lines

.paè.fo                            Listing 1
                            Listing 1

elijah-brown father-of robert-brown-sr
robert-brown-sr father-of robert-brown-jr
john-mccollister father-of lavenia-mccollister
isam-mccollister father-of john-mccollister
mr-holt father-of bettie-holt
elias-presley father-of margret-presley
robert-brown-jr father-of robert-brown-iii
paul-h-sewall father-of virginia-sewall
paul-h-sewall father-of paul-sewall-jr
paul-sewall-jr father-of peter-sewall
paul-sewall-jr father-of dee-dee-sewall
paul-sewall-jr father-of mark-sewall
paul-sewall-jr father-of paul-sewall-iii
robert-brown-jr father-of kenneth-brown
robert-brown-sr father-of amos-trice-brown
robert-brown-sr father-of james-elro-brown
clarence-bailey-compton father-of elanor-compon
george-washington-compton father-of clarence-bailey-compton
samuel-compton father-of george-washington-compton
henry-sewall father-of paul-h-sewall
dr-james-d-nelson father-of rachel-nelson
robert-sewall father-of henry-sewall
paul-hebert father-of evelina-hebert
harry-breeden father-of X if
         dorothy-wallace mother-of X
berke-breeden father-of harry-breeden
john-wallace father-of dorothy-wallace
robert-brown-iii father-of krystl-raquelle-brown
paul-sewall-jr father-of robert-sewall-ii
danny-crider father-of amy-crider
bill-skirvin father-of marty-skirvin
bill-skirvin father-of rodney-skirvin
tommy-breeden father-of thomas-andrew-breeden
tommy-breeden father-of suzanne-breeden
john-alsop father-of joy-alsop
lester-stevens father-of geneva-stevens
strawder-breeden father-of daren-breeden
daren-breeden father-of shaun-breeden
strawder-breeden father-of deidra-breeden
robert-bishop father-of krystal-bishop
robert-bishop father-of tiffany-bishop
robert-brown-sr father-of opal-brown
strawder-breeden father-of deva-breeden
strawder-breeden father-of stephanie-breeden
johnny-wilson father-of jonathan-wilson
lester-stevens father-of geneva-stevens
bettie-holt mother-of lavenia-mccollister
miss-hornsby mother-of robert-brown-sr
elizabeth-arthur mother-of john-mccollister
margret-e-presley mother-of betty-holt
virginia-sewall mother-of robert-brown-iii
elanor-compton mother-of virginia-sewall
.paèlilian-givens mother-of X if
         paul-sewall-jr father-of X
virginia-sewall mother-of kenneth-brown
lavenia-mccollister mother-of amos-trice-brown
lavenia-mccollister mother-of james-elro-brown
sarah-virginia-sanford mother-of elanor-compton
mary-eliza-sanford mother-of clarence-bailey-compton
rachel-nelson mother-of paul-h-sewall
jane-kirk mother-of rachel-nelson
evelina-hebert mother-of henry-sewall
eugina-hamilton mother-of evelina-hebert
dorothy-wallace mother-of darlene-breeden
dorothy-wallace mother-of willena-breeden
dorothy-wallace mother-of karen-breeden
dorothy-wallace mother-of bonnie-breeden
dorothy-wallace mother-of tommy-breeden
dorothy-wallace mother-of dorothy-breeden
dorothy-wallace mother-of brenda-breeden
dorothy-wallace mother-of betty-breeden
dorothy-wallace mother-of strawder-breeden
flo-marsh mother-of harry-breeden
christine-xxx mother-of dorothy-wallace
darlene-breeden mother-of krystl-raquelle-brown
dorothy-breeden mother-of amy-crider
brenda-breeden mother-of X if
         bill-skirvin father-of X
joy-alsop mother-of suzanne-breeden
joy-alsop mother-of thomas-andrew-breeden
pauline-davis mother-of joy-alsop
myrtle-jackson mother-of geneva-stevens
tammy-xxx mother-of shaun-breeden
deidra-breeden mother-of krystal-bishop
deidra-breeden mother-of tiffany-bishop
lavenia-mccollister mother-of opal-brown
lavenia-mccollister mother-of robert-brown-jr
elanor-compton mother-of paul-sewall-jr
karen-breeden mother-of jonathan-wilson
geneva-stevens mother-of X if
         strawder-breeden father-of X
myrtle-jackson mother-of geneva-stevens
male (X) if
         X father-of Y
male (john-viscar)
male (shaun-breeden)
female (X) if
         X mother-of Y
female (willena-breeden)
female (bonnie-breeden)
female (karen-breeden)
female (betty-breeden)
female (judy-tracey)
X wife Y if
         X mother-of Z and
         Y father-of Z
èX husband Y if
         Y wife X
X parent-of Y if
         X father-of Y
X parent-of Y if
         X mother-of Y
X wife-of Y if
         X wife Y
judy-tracy wife-of tommy-breeden
X husband-of Y if
         X husband Y
john-viscar husband-of pauline-davis
X child-of Y if
         Y parent-of X
X descendant-of Y if
         X child-of Y
X descendant-of Y if
         Z child-of Y and
         X descendant-of Z
X ancestor-of Y if
         X parent-of Y
X ancestor-of Y if
         Z parent-of Y and
         X ancestor-of Z
lavenia-mccollister moher-of robert-brown-jr
X sibling-of Y if
         Z mother-of X and
         Z mother-of Y and
         x father-of X and
         x father-of Y and
         Not (X EQ Y)
X half-sibling-of Y if
         Z mother-of X and
         Z mother-of Y and
         Not (X sibling-of Y) and
         Not (X EQ Y)
X half-sibling-of Y if
         Z father-of X and
         Z father-of Y and
         Not (X sibling-of Y) and
         Not (X EQ Y)
X aunt-or-uncle-of Y if
         Z parent-of Y and
         X sibling-of Z
X cousin-of Y if
         Z aunt-or-uncle-of X and
         Y child-of Z
.paè
                           Figure 1
.fo                           Figure 1

which (X X father-of robert-brown-iii)
Answer is robert-brown-jr
No (more) answers

which (X robert-brown-iii father-of X)
Answer is krystl-raquelle-brown
No (more) answers

which (X X parent-of krystl-raquelle-brown)
Answer is robert-brown-iii
Answer is darlene-breeden
No (more) answers

which (X X descendant-of robert-brown-sr)
Answer is robert-brown-jr
Answer is amos-trice-brown
Answer is james-elro-brown
Answer is opal-brown
Answer is robert-brown-iii
Answer is kenneth-brown
Answer is krystl-raquelle-brown
No (more) answers

which (X X aunt-or-uncle-of robert-brown-iii)
Answer is amos-trice-brown
Answer is james-elro-brown
Answer is opal-brown
Answer is paul-sewall-jr
No (more) answers

which (X X aunt-or-uncle-of krystl-raquelle-brown)
Answer is kenneth-brown
Answer is willena-breeden
Answer is karen-breeden
Answer is bonnie-breeden
Answer is tommy-breeden
Answer is dorothy-breeden
Answer is brenda-breeden
Answer is betty-breeden
Answer is strawder-breeden
No (more) answers

which (X robert-brown-iii cousin-of X)
Answer is peter-sewall
Answer is dee-dee-sewall
Answer is mark-sewall
Answer is paul-sewall-iii
Answer is robert-sewall-ii
No (more) answers
.paèwhich (X krystl-raquelle-brown cousin-of X)
Answer is jonathan-wilson
Answer is thomas-andrew-breeden
Answer is suzanne-breeden
Answer is amy-crider
Answer is marty-skirvin
Answer is rodney-skirvin
Answer is daren-breeden
Answer is deidra-breeden
Answer is deva-breeden
Answer is stephanie-breeden
No (more) answers
.paè                            Listing 2
.fo                             Listing 2

((cousin-of X Y)
  (aunt-or-uncle-of Z X)
  (child-of Y Z))
((aunt-or-uncle-of X Y)
  (parent-of Z Y)
  (sibling-of X Z))
((half-sibling-of X Y)
  (mother-of Z X)
  (mother-of Z Y)
  (NOT ? ((sibling-of X Y)))
  (NOT ? ((EQ X Y))))
((half-sibling-of X Y)
  (father-of Z X)
  (father-of Z Y)
  (NOT ? ((sibling-of X Y)))
  (NOT ? ((EQ X Y))))
((male X)
  (father-of X Y))
((male john-viscar))
((male shaun-breeden))
((female X)
  (mother-of X Y))
((female willena-breeden))
((female bonnie-breeden))
((female karen-breeden))
((female betty-breeden))
((female judy-tracey))
((wife-of X Y)
  (wife X Y))
((wife-of judy-tracy tommy-breeden))
((wife X Y)
  (mother-of X Z)
  (father-of Y Z))
((husband X Y)
  (wife Y X))
((husband-of X Y)
  (husband X Y))
((husband-of john-viscar pauline-davis))
((descendant-of X Y)
  (child-of X Y))
((descendant-of X Y)
  (child-of Z Y)
  (descendant-of X Z))
((child-of X Y)
  (parent-of Y X))
((parent-of X Y)
  (father-of X Y))
((parent-of X Y)
  (mother-of X Y))
.paè((ancestor-of X Y)
  (parent-of X Y))
((ancestor-of X Y)
  (parent-of Z Y)
  (ancestor-of X Z))
((moher-of lavenia-mccollister robert-brown-jr))
((father-of elijah-brown robert-brown-sr))
((father-of robert-brown-sr robert-brown-jr))
((father-of john-mccollister lavenia-mccollister))
((father-of isam-mccollister john-mccollister))
((father-of mr-holt bettie-holt))
((father-of elias-presley margret-presley))
((father-of robert-brown-jr robert-brown-iii))
((father-of paul-h-sewall virginia-sewall))
((father-of paul-h-sewall paul-sewall-jr))
((father-of paul-sewall-jr peter-sewall))
((father-of paul-sewall-jr dee-dee-sewall))
((father-of paul-sewall-jr mark-sewall))
((father-of paul-sewall-jr paul-sewall-iii))
((father-of robert-brown-jr kenneth-brown))
((father-of robert-brown-sr amos-trice-brown))
((father-of robert-brown-sr james-elro-brown))
((father-of clarence-bailey-compton elanor-compon))
((father-of george-washington-compton clarence-bailey-compton))
((father-of samuel-compton george-washington-compton))
((father-of henry-sewall paul-h-sewall))
((father-of dr-james-d-nelson rachel-nelson))
((father-of robert-sewall henry-sewall))
((father-of paul-hebert evelina-hebert))
((father-of harry-breeden X)
  (mother-of dorothy-wallace X))
((father-of berke-breeden harry-breeden))
((father-of john-wallace dorothy-wallace))
((father-of robert-brown-iii krystl-raquelle-brown))
((father-of paul-sewall-jr robert-sewall-ii))
((father-of danny-crider amy-crider))
((father-of bill-skirvin marty-skirvin))
((father-of bill-skirvin rodney-skirvin))
((father-of tommy-breeden thomas-andrew-breeden))
((father-of tommy-breeden suzanne-breeden))
((father-of john-alsop joy-alsop))
((father-of lester-stevens geneva-stevens))
((father-of strawder-breeden daren-breeden))
((father-of daren-breeden shaun-breeden))
((father-of strawder-breeden deidra-breeden))
((father-of robert-bishop krystal-bishop))
((father-of robert-bishop tiffany-bishop))
((father-of robert-brown-sr opal-brown))
((father-of strawder-breeden deva-breeden))
((father-of strawder-breeden stephanie-breeden))
((father-of johnny-wilson jonathan-wilson))
((father-of lester-stevens geneva-stevens))
((mother-of bettie-holt lavenia-mccollister))
((mother-of miss-hornsby robert-brown-sr))
((mother-of elizabeth-arthur john-mccollister))è((mother-of margret-e-presley betty-holt))
((mother-of virginia-sewall robert-brown-iii))
((mother-of elanor-compton virginia-sewall))
((mother-of lilian-givens X)
  (father-of paul-sewall-jr X))
((mother-of virginia-sewall kenneth-brown))
((mother-of lavenia-mccollister amos-trice-brown))
((mother-of lavenia-mccollister james-elro-brown))
((mother-of sarah-virginia-sanford elanor-compton))
((mother-of mary-eliza-sanford clarence-bailey-compton))
((mother-of rachel-nelson paul-h-sewall))
((mother-of jane-kirk rachel-nelson))
((mother-of evelina-hebert henry-sewall))
((mother-of eugina-hamilton evelina-hebert))
((mother-of dorothy-wallace darlene-breeden))
((mother-of dorothy-wallace willena-breeden))
((mother-of dorothy-wallace karen-breeden))
((mother-of dorothy-wallace bonnie-breeden))
((mother-of dorothy-wallace tommy-breeden))
((mother-of dorothy-wallace dorothy-breeden))
((mother-of dorothy-wallace brenda-breeden))
((mother-of dorothy-wallace betty-breeden))
((mother-of dorothy-wallace strawder-breeden))
((mother-of flo-marsh harry-breeden))
((mother-of christine-xxx dorothy-wallace))
((mother-of darlene-breeden krystl-raquelle-brown))
((mother-of dorothy-breeden amy-crider))
((mother-of brenda-breeden X)
  (father-of bill-skirvin X))
((mother-of joy-alsop suzanne-breeden))
((mother-of joy-alsop thomas-andrew-breeden))
((mother-of pauline-davis joy-alsop))
((mother-of myrtle-jackson geneva-stevens))
((mother-of tammy-xxx shaun-breeden))
((mother-of deidra-breeden krystal-bishop))
((mother-of deidra-breeden tiffany-bishop))
((mother-of lavenia-mccollister opal-brown))
((mother-of lavenia-mccollister robert-brown-jr))
((mother-of elanor-compton paul-sewall-jr))
((mother-of karen-breeden jonathan-wilson))
((mother-of geneva-stevens X)
  (father-of strawder-breeden X))
((mother-of myrtle-jackson geneva-stevens))
((sibling-of X Y)
  (mother-of Z X)
  (mother-of Z Y)
  (father-of x X)
  (father-of x Y)
  (NOT ? ((EQ X Y))))
.paè                            Listing 3
.fo                             Listing 3

(DEFUN * (NLAMBDA X
  NIL ))

(¬ Thσ functioε (CAA╥ X⌐ mean≤ (CA╥ (CA╥ X))«  Thi≤ conventioε i≤ ì
extendeΣ t∩ (CDA╥ X⌐ mean≤ (CD╥ (CA╥ X))¼ etc« *)

(DEFUN CONCAT (LAMBDA (P Q)
  (* concatenate 2 lists *)
  ((NULL P) Q)
  (CONS (CAR P) (CONCAT (CDR P) Q)) ))

(DEFUN PURGE (LAMBDA (L)
  (* purge a list of duplicate members *)
  ((NULL L) NIL)
  ((MEMBER (CAR L) (CDR L))
    (PURGE (CDR L)) )
  (CONS (CAR L) (PURGE (CDR L))) ))

(DEFUN JOIN (LAMBDA (L M)
  (* form the set union of 2 lists *)
  (PURGE (CONCAT L M)) ))

(DEFUN MEET (LAMBDA (L M)
  (* form the set intersection of 2 lists *)
  (PURGE (COMMON L M)) ))

(DEFUN COMMON (LAMBDA (L M)
  (* form the set intersection of 2 lists with possible
      duplicate entries *)
  ((NULL L) NIL)
  ((MEMBER (CAR L) M)
    (CONS (CAR L) (COMMON (CDR L) M)) )
  (COMMON (CDR L) M) ))

(DEFUN DEF (LAMBDA (V E)
  (* determine whether the variable V is defined in the
      environment E *)
  ((NULL E) NIL)
  ((EQUAL V (CAAR E)) T)
  (DEF V (CDR E)) ))

(DEFUN IMM (LAMBDA (V E)
  (* return the immediate successor of the variable V in the
      environment E *)
  ((NULL E) NIL)
  ((EQUAL V (CAAR E))
    (CDAR E) )
  (IMM V (CDR E)) ))
.paè(DEFUN ULT (LAMBDA (V E)
  (* return the ultimate successor of the variable V in the
      environment E *)
  ((DEF V E)
    (ULT (IMM V E) E) )
  V ))

(DEFUN PAIRP (LAMBDA (P)
  (* determine if P is a pair (not an atom) *)
  ((ATOM P) NIL)
  T ))

(DEFUN VARIABLEP (LAMBDA (V)
  (* determine if V is a variable *)
  (EQ (CAR (UNPACK V)) '*) ))

(DEFUN RECREAL (LAMBDA (F E)
  (* return the recursive realization of a formula F in the
      environment E which amounts to instantiating all variables
      from the environment *)
  ((PAIRP F)
    (CONS (RECREAL (CAR F) E) (RECREAL (CDR F) E)) )
  ((DEF F E)
    (RECREAL (ULT F E) E) )
  F ))

(DEFUN OCCURS (LAMBDA (V X E)
  (* see if the variable V occurs in the term X under the
      environment E *)
  ((VARIABLEP X)
    ((DEF X E)
      (OCCURS V (IMM X E) E) )
    ((EQ V X) T) )
  ((ATOM X) NIL)
  ((OCCURS V (CAR X) E) T)
  (OCCURS V (CDR X) E) ))

(DEFUN UNIFY (LAMBDA (A B E)
  (* unify 2 expressions (A and B) in the environment E by
      extending E to the most general unifier of A and B and
      returning that environment *)
  ((EQ E 'IMPOSSIBLE)
    'IMPOSSIBLE )
  (EQUATE (ULT A E) (ULT B E) E) ))
.paè(DEFUN EQUATE (LAMBDA (A B E)
  (* auxilliary routine to UNIFY so that the flow of control
      ping-pongs recursivly between UNIFY and EQUATE to
      construct the most general unifier of A and B *)
  ((EQUAL A B) E)
  ((VARIABLEP A)
    ((OCCURS A B E)
      'IMPOSSIBLE )
    (CONS (CONS A B) E) )
  ((VARIABLEP B)
    ((OCCURS B A E)
      'IMPOSSIBLE )
    (CONS (CONS B A) E) )
  ((ATOM A)
    'IMPOSSIBLE )
  ((ATOM B)
    'IMPOSSIBLE )
  (UNIFY (CDR A) (CDR B) (UNIFY (CAR A) (CAR B) E)) ))

(DEFUN VARS (LAMBDA (X)
  (* return a list of all the variables found in the expression
      X *)
  ((NULL X) NIL)
  ((VARIABLEP X) X)
  ((ATOM X) NIL)
  (CONCAT (VARS (CAR X)) (VARS (CDR X))) ))

(DEFUN VARIANT (LAMBDA (Q E D)
  (* returns a variant of D such that all variables are distinct
      from those of Q in the environment E *)
  (RECREAL D (MAKENV (VARS Q) (VARS E) (VARS D))) ))

(DEFUN MAKENV (LAMBDA (Q E D)
  (* make an environment such that the instantiation of D in
      this environment will have no variables in common with the
      instantiation of Q in E *)
  (MAKENV1 (MEET D (JOIN Q E)) (JOIN (JOIN Q E) D)) ))

(DEFUN MAKENV1 (LAMBDA (P Q V)
  (* does the dirty work for MAKENV and VARIANT by generating an
      environment that sticks asterisks onto the front of all
      variable names in Q that also occur in P (V is a local
      temporary variable) *)
  ((NULL P) NIL)
  ((ATOM P)
    (SETQ V P)
    (LOOP
      ((NOT (MEMBER V Q)))
      (SETQ V (PACK (CONS '* (UNPACK V)))) )
    (CONS P V) )
  (CONS (MAKENV1 (CAR P) Q) (MAKENV1 (CDR P) Q)) ))
.paè(DEFUN GETLIT (LAMBDA (CL N)
  (* get the Nth litteral in the clause CL and return it both as
      the functions value and in the free variable LITG along
      with its sign in the free variable SIGNG *)
  (SETQ LITG (CAR (NTH CL N)))
  (SETQ SIGNG (NOT (EQ (CAR LITG) '~)))
  ((NOT (NULL SIGNG)) LITG)
  (CADR LITG) ))

(DEFUN FRONT (LAMBDA (C N)
  (* return all elements in the clause C in front of element N
      *)
  ((NULL C) NIL)
  ((ZEROP N) NIL)
  ((EQ N 1) NIL)
  (CONS (CAR C) (FRONT (CDR C) (SUB1 N))) ))

(DEFUN BACK (LAMBDA (C N)
  (* return all elements in clause C in back of element N *)
  (NTH C (ADD1 N)) ))

(DEFUN FACTOR (LAMBDA (C P1 N1 S1 P2 N2 S2 ENV)
  (* returns a factored version of the clause C *)
  (SETQ ENV 'IMPOSSIBLE)
  (SETQ N1 0)
  (LOOP
    (SETQ N1 (ADD1 N1))
    ((GREATERP N1 (LENGTH C))
      'IMPOSSIBLE )
    (GETLIT C N1)
    (SETQ P1 LITG)
    (SETQ S1 SIGNG)
    (SETQ N2 N1)
    ( ((LOOP
          (SETQ N2 (ADD1 N2))
          ((GREATERP N2 (LENGTH C)))
          (GETLIT C N2)
          (SETQ P2 LITG)
          (SETQ S2 SIGNG)
          ( ((EQ S1 S2)
              (SETQ ENV (UNIFY P1 P2)) ) )
          ((NOT (EQ ENV 'IMPOSSIBLE))
            (SETQ C (RECREAL C ENV))
            (SETQ C (APPEND (FRONT C N1) (BACK C N1))) ) )) )
    ((NOT (EQ ENV 'IMPOSSIBLE))) )
  ((NOT (EQ ENV 'IMPOSSIBLE)) C)
  'IMPOSSIBLE ))
.paè(DEFUN BINRES (LAMBDA (CL1 N1 CL2 N2 ENV LIT1 SGN1 LIT2 SGN2 L1
    L2 LITG SIGNG)
  (* compute the binary resolvent of clause CL1 litteral number
      N1 with clause CL2 litteral number N2 and return the
      instantiated resolvent *)
  (SETQ CL2 (VARIANT CL1 ENV CL2))
  (SETQ LIT1 (GETLIT CL1 N1))
  (SETQ L1 LITG)
  (SETQ SGN1 SIGNG)
  (SETQ LIT2 (GETLIT CL2 N2))
  (SETQ L2 LITG)
  (SETQ SGN2 SIGNG)
  ((EQ SGN1 SGN2) NIL)
  (SETQ ENV (UNIFY LIT1 LIT2 ENV))
  ((EQ ENV 'IMPOSSIBLE)
    'IMPOSSIBLE )
  (RECREAL (APPEND (FRONT CL1 N1) (BACK CL1 N1) (FRONT CL2 N2)
      (BACK CL2 N2)) ENV) ))

(DEFUN PARAMOD (LAMBDA (FROM INTO PF F PI I SEL SUB ENV SWAP PM)
  (* return the paramodulant of the FROM clause into the INTO
      clause *)
  (SETQ INTO (VARIANT FROM NIL INTO))
  (SETQ PM 'IMPOSSIBLE)
  (SETQ PF 0)
  (LOOP
    (SETQ PF (ADD1 PF))
    (SETQ F (CAR (NTH FROM PF)))
    ((NULL F))
    ((EQ (CAR F) '=)
      (SETQ SEL (CADR F))
      (SETQ SUB (CADDR F))
      (SETQ PI 0)
      (LOOP
        (SETQ PI (ADD1 PI))
        (SETQ I (CAR (NTH INTO PI)))
        ((NULL I))
        (SETQ ENV (UNIFY SEL I))
        ( ((EQ ENV 'IMPOSSIBLE)
            (SETQ ENV (UNIFY SUB I))
            (SETQ SUB SEL) ) )
        ((NOT (EQ ENV 'IMPOSSIBLE))
          (SETQ FROM (RECREAL FROM ENV))
          (SETQ INTO (RECREAL INTO ENV))
          ( ((NOT (NULL SWAP))
              (SETQ SUB SEL) ) )
          (SETQ INTO (APPEND (FRONT INTO PI) (LIST SUB) (BACK
              INTO PI)))
          (SETQ FROM (APPEND (FRONT FROM PF) (BACK FROM PF)))
          (SETQ PM (APPEND FROM INTO)) ) ) )
    ((NOT (EQ PM 'IMPOSSIBLE))) )
  PM ))
.paè                           Figure 2
.fo                            Figure 2

(SETQ C1 '((F *X)))
((F *X))
(SETQ C2 '((G *X)))
((G *X))
(SETQ E (UNIFY C1 C2))
IMPOSSIBLE
(RECREAL C1 E)
((F *X))
(RECREAL C2 E)
((G *X))

(SETQ C2 '((F A)))
((F A))
(SETQ E (UNIFY C1 C2))
((*X . A))
(RECREAL C1 E)
((F A))
(RECREAL C2 E)
((F A))

(SETQ C2 '((F (G *Y))))
((F (G *Y)))
(SETQ E (UNIFY C1 C2))
((*X G *Y))
(RECREAL C1 E)
((F (G *Y)))
(RECREAL C2 E)
((F (G *Y)))

(SETQ C2 '((F (F *X))))
((F (F *X)))
(SETQ E (UNIFY C1 C2))
IMPOSSIBLE
(RECREAL C1 E)
((F *X))
(RECREAL C2 E)
((F (F *X)))

(SETQ C1 '((F *X A) (G B *Y)))
((F *X A) (G B *Y))
(SETQ C2 '((F B *Y) (G *X *Z)))
((F B *Y) (G *X *Z))
(SETQ E (UNIFY C1 C2))
((*Z . A) (*Y . A) (*X . B))
(RECREAL C1 E)
((F B A) (G B A))
(RECREAL C2 E)
((F B A) (G B A))
.paè                           Figure 3
.fo                            Figure 3

(SETQ CL1 '((F *X) (~ (G *Y A)) (F B)))
((F *X) (~ (G *Y A)) (F B))

(FACTOR CL1)
((~ (G *Y A)) (F B))

(SETQ CL2 '((G B *X) (F *Y)))
((G B *X) (F *Y))

(BINRES CL1 2 CL2 1)
((F *X) (F B) (F **Y))

(SETQ FROM '((F *X) (= (G *Y A) (F *Y)) (F B)))
((F *X) (= (G *Y A) (F *Y)) (F B))

(SETQ INTO CL2)
((G B *X) (F *Y))

(PARAMOD FROM INTO)
((F *X) (F B) (F *Y) (F **Y))
.paè                            Listing 4
.fo                             Listing 4

(DEFUN VARIABLEP (LAMBDA (V)
  (* determine if V is a variable: if it starts with lower-case
      it is *)
  ((ATOM V)
    (GREATERP (ASCII (CAR (UNPACK V))) (ASCII `)) )
  NIL ))

(DEFUN LPAR (LAMBDA (R)
  (* return left parent *)
  (CAR R) ))

(DEFUN LLIT# (LAMBDA (R)
  (* return left litteral number *)
  (CADR R) ))

(DEFUN RPAR (LAMBDA (R)
  (* return right parent *)
  (CADDR R) ))

(DEFUN RLIT# (LAMBDA (R)
  (* return right litteral number *)
  (CAR (CDDDR R)) ))

(DEFUN NLITS (LAMBDA (R)
  (* return number of litterals *)
  (CADR (CDDDR R)) ))

(DEFUN MAXNDX (LAMBDA (R)
  (* return maximum index *)
  (CADDR (CDDDR R)) ))

(DEFUN BINDINGS (LAMBDA (R)
  (* return the bindings *)
  (CAR (CDDDR (CDDDR R))) ))

(DEFUN SETLPAR (LAMBDA (R V)
  (* set left parent *)
  (RPLACA R V) ))

(DEFUN SETLLIT# (LAMBDA (R V)
  (* set left litteral number *)
  (RPLACA (CDR R) V) ))

(DEFUN SETRPAR (LAMBDA (R V)
  (* set right parent *)
  (RPLACA (CDDR R) V) ))

(DEFUN SETRLIT# (LAMBDA (R V)
  (* set right litteral number *)
  (RPLACA (CDDDR R) V) ))
.paè(DEFUN SETNUMLITS (LAMBDA (R V)
  (* set number of litterals *)
  (RPLACA (CDR (CDDDR R)) V) ))

(DEFUN SETMAXNDX (LAMBDA (R V)
  (* set maximum index *)
  (RPLACA (CDDR (CDDDR R)) V) ))

(DEFUN SETBINDINGS (LAMBDA (R V)
  (* set bindings *)
  (RPLACA (CDDDR (CDDDR R)) V) ))

(DEFUN INRECP (LAMBDA (R)
  (* is R an input record? *)
  (NULL (RPAR R)) ))

(DEFUN LEQP (LAMBDA (X Y)
  (* is X less than or equal to Y ? *)
  (NOT (GREATERP X Y)) ))

(DEFUN NMEMS (LAMBDA (L)
  (* return the number of members in the list L *)
  ((NULL L) 0)
  (ADD1 (NMEMS (CDR L))) ))

(DEFUN EXTRACT (LAMBDA (K L TMP)
  (* return the Kth member of L *)
  (* TMP is a local variable *)
  (LOOP
    ((ZEROP K) TMP)
    (SETQ K (SUB1 K))
    (SETQ TMP (POP L)) ) ))

(DEFUN RESOLVE (LAMBDA (CL1 I CL2 J LLIT RLIT LNDX RNDX BNDEV
    LSIGN RSIGN)
  (* resolve clause CL1 litteral I with clause CL2 litteral J
      returning a new clause record representing the resolvent:
      UNIFY will extend the binding environment: returns NIL if
      impossible *)
  (GETLIT CL1 I)
  (SETQ LLIT LITG)
  (SETQ LNDX INDEXG)
  (SETQ LSIGN SIGNG)
  (GETLIT CL2 J)
  (SETQ RLIT LITG)
  (SETQ RNDX (PLUS INDEXG (MAXNDX CL1)))
  (SETQ RSIGN SIGNG)
  (* create the new clause record *)
  (SETQ BNDEV (LIST CL1 I CL2 J (DIFFERENCE (PLUS (NLITS CL1)
      (NLITS CL2)) 2) (PLUS (MAXNDX CL1) (MAXNDX CL2)) NIL))
  (* test for opposite signs *)
  ((EQ LSIGN RSIGN) NIL)
  (* extend the environment by the unification algorithm *)
  ((UNIFY LLIT LNDX RLIT RNDX) BNDEV)
  NIL ))è
(DEFUN GETLIT (LAMBDA (CL K)
  (* get the Kth litteral in clause CL: return the litteral
      gotten in LITG: and the associated index in INDEXG *)
  (* if CL is an input clause then extract the Kth litteral and
      set the index to 1 *)
  ((INRECP CL)
    (SETQ LITG (EXTRACT K (LPAR CL)))
    (SETQ SIGNG (EQ K 1))
    (SETQ INDEXG 1) )
  (* if it is in the left parent of the clause then get the
      litteral from the left parent *)
  (* this is true if K is less than the litteral last resolved
      upon in the left parent of the current clause *)
  ((LESSP K (LLIT# CL))
    (GETLIT (LPAR CL) K) )
  (* this is also true if K is less than the number of litterals
      in the left parent but in this case we must adjust K by 1
      *)
  ((LESSP K (NUMLITS (LPAR CL)))
    (GETLIT (LPAR CL) (ADD1 K)) )
  (* if the selected litteral is in the right parent but left of
      the litteral last resolved upon then get the litteral from
      the right parent with the appropriate adjustment to K *)
  ((LESSP K (PLUS (SUB1 (NUMLITS (LPAR CL))) (RLIT# CL)))
    (GETLIT (RPAR CL) (ADD1 (DIFFERENCE K (NUMLITS (LPAR CL)))))
    (* in this case adjust the index got *)
    (SETQ INDEXG (PLUS INDEXG (MAXNDX (LPAR CL)))) )
  (* otherwise the selected litteral is in the right parent to
      the right of last litteral resolved upon so adjust K
      accordingly and get the litteral *)
  (GETLIT (RPAR CL) (PLUS (DIFFERENCE K (NUMLITS (LPAR CL))) 2))
  (* and adjust the index gotten *)
  (SETQ INDEXG (PLUS INDEXG (MAXNDX (LPAR CL)))) ))
.paè(DEFUN UNIFY (LAMBDA (TERM1 INDEX1 TERM2 INDEX2)
  (* attempt to unify TERM1 under INDEX1 with TERM2 under INDEX2
      and extend the binding environment represented in the
      global variable BNDEV: return T if successful or NIL if the
      unification is impossible *)
  (* if both terms and indices are equal then return T: no
      extension to BNDEV is needed *)
  ((EQUAL TERM1 TERM2)
    (EQ INDEX1 INDEX2)
    T )
  (* if TERM1 is a variable *)
  ((VARIABLEP TERM1)
    (* then if it is bound in the current environment *)
    ((ISBOUND TERM1 INDEX1 BNDEV)
      (* then substitute that binding and attempt to unify again
          *)
      (UNIFY TERMB INDEXB TERM2 INDEX2) )
    (* else if the variable of TERM1 occurs in TERM2 then we
        have a recursive """black" "hole""" situation so return
        NIL *)
    ((OCCUR TERM1 INDEX1 TERM2 INDEX2) NIL)
    (* else force a unification by adding the necessary binding
        and return T for success *)
    (BIND TERM1 INDEX1 TERM2 INDEX2 BNDEV)
    T )
  (* if TERM2 is a variable then swap the 2 terms and UNIFY the
      other way *)
  ((VARIABLEP TERM2)
    (UNIFY TERM2 INDEX2 TERM1 INDEX1) )
  (* otherwise if the heads of the terms unify then return the
      result of unifying the tails of the terms: the environment
      is extended as needed *)
  ((UNIFY (CAR TERM1) INDEX1 (CAR TERM2) INDEX2)
    (UNIFY (CDR TERM1) INDEX1 (CDR TERM2) INDEX2) ) ))
.paè(DEFUN ISBOUND (LAMBDA (VAR INDEX BNDEV)
  (* determine if the variable VAR under the index INDEX is
      bound in the binding environment BNDEV: if it is then
      return T and set the free variables TERMB and INDEXB to
      the term and index respectively to which it is bound: *)
  (* otherwise return NIL and do not alter the values of TERMB and
      INDEXB *)
  (* if BNDEV is an input record then it cannot be bound so
      return NIL *)
  ((INRECP BNDEV) NIL)
  (* if VAR under INDEX is equal to the head of the binding
      environment at this level then return T and set TERMB and
      INDEXB accordingly *)
  ((EQUAL (CONS VAR INDEX) (CAR (BINDINGS BNDEV)))
    (SETQ TERMB (CADAR (BINDINGS BNDEV)))
    (SETQ INDEXB (CAR (CDDAR (BINDINGS BNDEV))))
    T )
  (* else see if it is bound in the tail of the binding
      environment at this level *)
  ((ISBOUND VAR INDEX (CDR (BINDINGS BNDEV))) T)
  (* if not then check INDEX to see whether to search the left
      or right parent binding environment *)
  ((LEQP INDEX (MAXNDX (LPAR BNDEV)))
    (* search left parent *)
    (ISBOUND VAR INDEX (LPAR BNDEV)) )
  (* search right parent *)
  ((ISBOUND VAR (DIFFERENCE INDEX (MAXNDX (LPAR BNDEV))) (RPAR
      BNDEV))
    (* adjust INDEXB accordingly *)
    (SETQ INDEXB (PLUS INDEXB (MAXNDX (LPAR BNDEV))))
    (* and return success *)
    T )
  (* all possible approaches failed so return NIL for not bound *)
  NIL ))
.paè(DEFUN OCCUR (LAMBDA (V I TERM J)
  (* see if the variable V under the index I occurs in the term
      TERM under the index J and return T or NIL *)
  (* if TERM is a variable *)
  ((VARIABLEP TERM)
    (* then if it is bound *)
    ((ISBOUND TERM J BNDEV)
      (* then make the substitution and test for occurance *)
      (OCCUR V I TERMB INDEXB) )
    (* if V equals TERM *)
    ((EQ V TERM)
      (* then return T if I=J else NIL *)
      (EQ I J) ) )
  (* if TERM is atomic and not a variable *)
  (* then it is a constant so return NIL *)
  ((ATOM TERM) NIL)
  (* otherwise if V under I occurs in the head of TERM under J
      then return T *)
  ((OCCUR V I (CAR TERM) J) T)
  (* otherwise return T if V under I occurs in the tail of TERM
      under J and NIL otherwise *)
  (OCCUR V I (CDR TERM) J) ))

(DEFUN BIND (LAMBDA (V I TERM J BNDEV)
  (* bind V under I to TERM under J in BNDEV *)
  (SETBINDINGS BNDEV (CONS (CONS (CONS V I) (CONS TERM J))
      (BINDINGS BNDEV))) ))

(DEFUN * (LAMBDA COMMENTS
  NIL ))

(DEFUN MAKECL (LAMBDA (CL)
  (* make a clause record out of the expression CL *)
  (LIST CL 0 NIL 0 (NMEMS CL) 1 NIL) ))
.paè                           Figure 4
.fo                            Figure 4

(SETQ CLAUSE-1 '((F x y) (G x) (P A y x) ))
((F x y) (G x) (P A y x))

(SETQ CLAUSE-2 '((P A B C)))
((P A B C))

(SETQ CLAUSE-3 '((G C)))
((G C))

(SETQ TEST (RESOLVE (MAKECL CLAUSE-1) 2 (MAKECL CLAUSE-3) 1))
(
      ( ((F x y) (G x) (P A y x)) 0 NIL 0 3 1 NIL )
      2
      ( ((G C)) 0 NIL 0 1 1 NIL )
      1
      2
      2
      ( ((x . 1) C . 2))
)